WebAssembly 形式手法
WebAssembyはIsabelle/HOLでwell-definedに定義されている$ ^{(1)}
ソースは↓に
WebAssembly - Archive of Formal Proofs. 2018-04-29
Coqの方でやっているものもある
GitHub: WasmCert/WasmCert-Coq: A mechanisation of Wasm in Coq
今はCoqで形式化している？
WebAssembly関連の論文
『Mechanising and Verifying the WebAssembly Specification』. 2018.
『Formal Methods and the WebAssembly Specification』. 2019.
Two Mechanisations of WebAssembly 1.0 | SpringerLink. 2021-11-10.
確認用
Q. WebAssembly 形式手法
参考
(1) 『Formal Methods and the WebAssembly Specification』. 2019.
『Mechanising and Verifying the WebAssembly Specification』. 2018.
関連
Isabelle